\section{Proof Process}

\begin{frame}
\frametitle{Proof Process of Projects}

\begin{itemize}
   \item Statistics:\\
    \begin{center}{\footnotesize
  	 \begin{tabular}{|c|c|c|c|}
		\hline
		 \textsl{Projects} &  \textsl{POs}	& \textsl{POs WD} &	\textsl{Total}\\
		\hline
		\textit{Power} & 	21 &	4 &	25\\
		\hline
		\textit{Types Library} &	22 &	68 &	90\\
		\hline
		\textit{Hardware Library} &	108 &	324 &	432\\
		\hline
		\textit{Z80} &	631	 & 2470 & 	3101\\
		\hline
		   &    &  & 		\textbf{3648}\\
		\hline
	 \end{tabular}
   }
	\end{center}

   \item Project Z80
    \begin{itemize}
	    \item  Approximately 25\% are not solved automatically
		\item Approximately 18 days are needed to make almost all the proofs using a
		single core computer
		\item Some proofs needed to be replayed when we make changes to the specification
	\end{itemize}
	\item The time of proof can be reduced using advanced features
	
	
\end{itemize}

\end{frame}


\begin{frame}
\frametitle{Proof Process - Advanced Features}

	\begin{itemize}
	\item Parallel theorem prover with 3 dual core computers 
	\item Two simple examples of user pass from theorem prover
	
 		\begin{itemize}
 		   \item Specific:\\
 		  	 $Pattern( x , y : dom(bitget) )$ \\ $\& ff(0) \& dd \& eh(dom(bitget)) \& ss \& pr;$\\
 		    \ldots
 		   \item General:\\
 		   	$Pattern( x : dom(y) )$ \\ $\& ff(0) \& dd \& eh(dom(y)) \& ss \& pr;$
         \end{itemize}
        
    \end{itemize}
    
\end{frame}



